Unbounded Proof-Length Speed-Up in Deduction Modulo
Identifieur interne : 004B56 ( Main/Exploration ); précédent : 004B55; suivant : 004B57Unbounded Proof-Length Speed-Up in Deduction Modulo
Auteurs : Guillaume Burel [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
English descriptors
Abstract
Abstract: In 1973, Parikh proved a speed-up theorem conjectured by Gödel 37 years before: there exist arithmetical formulæ that are provable in first order arithmetic, but whose shorter proof in second order arithmetic is arbitrarily smaller than any proof in first order. On the other hand, resolution for higher order logic can be simulated step by step in a first order narrowing and resolution method based on deduction modulo, whose paradigm is to separate deduction and computation to make proofs clearer and shorter. We prove that i + 1-th order arithmetic can be linearly simulated into i-th order arithmetic modulo some confluent and terminating rewrite system. We also show that there exists a speed-up between i-th order arithmetic modulo this system and i-th order arithmetic without modulo. All this allows us to prove that the speed-up conjectured by Gödel does not come from the deductive part of the proofs, but can be expressed as simple computation, therefore justifying the use of deduction modulo as an efficient first order setting simulating higher order.
Url:
DOI: 10.1007/978-3-540-74915-8_37
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001168
- to stream Istex, to step Curation: 001152
- to stream Istex, to step Checkpoint: 000F41
- to stream Hal, to step Corpus: 005027
- to stream Hal, to step Curation: 005027
- to stream Hal, to step Checkpoint: 003865
- to stream Main, to step Merge: 004C90
- to stream Main, to step Curation: 004B56
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Unbounded Proof-Length Speed-Up in Deduction Modulo</title><author><name sortKey="Burel, Guillaume" sort="Burel, Guillaume" uniqKey="Burel G" first="Guillaume" last="Burel">Guillaume Burel</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:4B57F783399002EC674355BAA2DFB99EA040FBFD</idno><date when="2007" year="2007">2007</date><idno type="doi">10.1007/978-3-540-74915-8_37</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-GV6VGFZB-D/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001168</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001168</idno><idno type="wicri:Area/Istex/Curation">001152</idno><idno type="wicri:Area/Istex/Checkpoint">000F41</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000F41</idno><idno type="wicri:doubleKey">0302-9743:2007:Burel G:unbounded:proof:length</idno><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:inria-00138195</idno><idno type="url">https://hal.inria.fr/inria-00138195</idno><idno type="wicri:Area/Hal/Corpus">005027</idno><idno type="wicri:Area/Hal/Curation">005027</idno><idno type="wicri:Area/Hal/Checkpoint">003865</idno><idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">003865</idno><idno type="wicri:Area/Main/Merge">004C90</idno><idno type="wicri:Area/Main/Curation">004B56</idno><idno type="wicri:Area/Main/Exploration">004B56</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Unbounded Proof-Length Speed-Up in Deduction Modulo</title><author><name sortKey="Burel, Guillaume" sort="Burel, Guillaume" uniqKey="Burel G" first="Guillaume" last="Burel">Guillaume Burel</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>Universitè Henri Poincarè & LORIA, Campus scientifique BP 239 — 54506 Vandœuvre-lès-Nancy Cedex</wicri:regionArea><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Vandœuvre-lès-Nancy</settlement></placeName></affiliation><affiliation></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="mix" xml:lang="en"><term>arithmetic</term><term>higher order logic</term><term>proof theory</term><term>proof-system translations</term><term>rewriting</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: In 1973, Parikh proved a speed-up theorem conjectured by Gödel 37 years before: there exist arithmetical formulæ that are provable in first order arithmetic, but whose shorter proof in second order arithmetic is arbitrarily smaller than any proof in first order. On the other hand, resolution for higher order logic can be simulated step by step in a first order narrowing and resolution method based on deduction modulo, whose paradigm is to separate deduction and computation to make proofs clearer and shorter. We prove that i + 1-th order arithmetic can be linearly simulated into i-th order arithmetic modulo some confluent and terminating rewrite system. We also show that there exists a speed-up between i-th order arithmetic modulo this system and i-th order arithmetic without modulo. All this allows us to prove that the speed-up conjectured by Gödel does not come from the deductive part of the proofs, but can be expressed as simple computation, therefore justifying the use of deduction modulo as an efficient first order setting simulating higher order.</div></front></TEI><affiliations><list><country><li>France</li></country><region><li>Grand Est</li><li>Lorraine (région)</li></region><settlement><li>Vandœuvre-lès-Nancy</li></settlement></list><tree><country name="France"><region name="Grand Est"><name sortKey="Burel, Guillaume" sort="Burel, Guillaume" uniqKey="Burel G" first="Guillaume" last="Burel">Guillaume Burel</name></region></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 004B56 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 004B56 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:4B57F783399002EC674355BAA2DFB99EA040FBFD
|texte= Unbounded Proof-Length Speed-Up in Deduction Modulo
}}
| This area was generated with Dilib version V0.6.33. |  |